da:fpf(Knd; k.Type), k:Knd.
normal-da{i:l}
normal-da(da)
 (fpf-dom(Kind-deq; k; da))
 normal-type{i:l}
 normal-type(fpf-cap(da; Kind-deq; k; void)) 

latex

Definitions	False, P  Q, A, t  T, x:A. B(x), b, b, , s = t, prop{i:l}, Knd, Type, x.A(x), x. t(x), top, fpf(A; a.B(a)), x:AB(x), Kind-deq, fpf-dom(eq; x; f), x:A  B(x), P  Q, P  Q, Unit, left + right, fpf-ap(f; eq; x), normal-type{i:l}(T), void, if b then t else f fi , fpf-all(A; eq; f; x,v.P(x;v)), fpf-cap(f; eq; x; z), normal-da{i:l}(da)
Lemmas	normal-type wf, fpf-ap wf, fpf wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, Knd wf, bool wf, bnot wf, not wf, assert wf